L:(Realizer List), B:Realizer. (AL. A || B)  (L) || B 

latex

Definitions	Top, P & Q, x. t(x), Y, reduce(f;k;as), (L), P  Q, Realizer, t  T, x:A. B(x), A c B, P  Q, x(s),
Lemmas	R-compat-Rplus-sq, l all cons, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, l member wf, R-compat wf, l all wf2, R-compat-none, es realizer wf